Quando definiamo un linguaggio di programmazione, fissiamo
1. Sintassi (programmi ben formati, escludendo espressioni senza senso)
2. Tipi (riduzione di programmi ammessi, escludendo errori comun)
3. Pragmatica (come usare costrutti e funzionalità)
4. Semantica (il significato logico di programmi ben formati)
Partiamo dalla sintassi.
La sintassi di un linguaggio formale definisce con rigore
1. L'alfabeto (quali simboli possono essere usati)
2. Struttura grammaticale dei programmi (quali combinazioni di simboli sono valide e quali vanno scartate)
Metodi standard di definire la sintassi sono ad esempio
- espressioni regolari (regex)
- gramatiche context-free
- notazione BNF
- diagrammi sintattici
- ...
Una grammatica BNF può essere ad esempio descrivere la struttura dei numeri interi
<numeral> ::= <digit> | <numeral> <digit>
<digit> ::= "0" | "1" | "2" | "3" | "4" | "5" | "6" | "7" | "8" | "9"
un <numeral> è una combinazione n-aria di <digit>.
I sistemi dei tipi sono costrutti sintattici che classificano espressioni secondo i tipi che esse calcolano. Essi associano tipi a ogni valore computato. Questo permette di evitare errori banali (effettuare operazioni aritmetiche su valori non numerici, o comunque qualsiasi operazione che non abbia definizione su un certa combinazione di tipi, per l'appunto). Ricapitolando:
1. Limitano l'occorrenza di errori
2. Permettono ottimizzazione a compile-time (ci sono spunti molto interessanti a riguardo sui design dei compilatori)
3. Riducono la presenza di bug
4. Scoraggiano pratiche sconsiderate
I sistemi di tipi sono spesso presentati come regole logiche. Chiaramente uno stesso linguaggio può avere tanti sistemi di tipi diversi.
Una simile formalizzazione non è solo bella da vedere, ma rende la vita facile a chiunque si approcci al linguaggio, dalla stesura al parsing fino alla compilazione. Vediamo alcuni vantaggi concreti:
- Standardizzazione del linguaggio: i programmatori scriveranno programmi sintatticamente corretti, gli implementatori scriveranno parser corretti
- Analisi formale delle proprietà del linguaggio: ambiguità, espressività, riconoscibilità, comparabilità
- Implementazione automatica del front-end di un compilatore: yacc, Bison, xtext, ...
Si prenda in considerazione l'alfabeto
A = { ( , ) }
Definire la grammatica per le stringhe di parentesi bilanciate
S ::= ?
I programmatori dovrebbero (sperabilmente) comprendere il codice che scrivono
Qualsiasi manuale di ogni linguaggio deve contenere una descrizione in linguaggio naturale dei vari costrutti (quindi una descrizione discorsiva in italiano o inglese, e non necessariamente definita usando formalismi computazionali), con esempi, frammenti di codice ed errori comuni
Chiamiamo questo insieme di elementi "pragmatics"
Si tratta di un'arte di fondamentale importanza, che va curata nella sua precisione e disambiguità. È arduo (se non impossibile) coprire tutti i casi, e diversi punti rimangono aperti ad interpretazione.
La parola semantica è stata introdotta nel 1900 per descrivere
lo studio di come le parole cambiano i loro significati (M. Bréal)
Ironicamente, il suo significato è cambiato trasformandosi così
lo studio del collegamento tra espressioni di un linguaggio (scritto, parlato, formale) e i loro significati. In informatica si occupa dello studio formale del significato di programmi ben formati.
Sono presenti diversi tipi di semantiche, che cadono (grossolanamente) in tre categorie:
1. Operazionali: interesse su come l'effetto è ottenuto
2. Denotazionali: interesse su cosa è l'effetto, indipendentemente da come questo sia ottenuto
3. Assiomatiche: interesse su asserzioni valide riguardo la computazione
Vediamo dunque di analizzare le tre categorie
Idea: definire un qualche tipo di macchina astratta e descrivere il significato di un programma in termini dei passaggi computazionali o istruzioni che la macchina esegue per svolgere il compito (enfasi sullo stato della macchina)
Si tratta di un formalismo molto indicato per spiegare la computazione
s0 -> s1 -> s2 -> ... -> sn -> r
Fondato negli anni 60 da John McCarthy esordendo con la sua famosissima pubblicazione scientifica del 1960 (Recursive Functions of Symbolic exressions and Their Computation by Machine) e Algol 68 (1975), crebbe negli anni 80 con l'introduzione dell'approccio SOS (Structural Operational Semantics) da perte di Gordon Plotkin con uno degli articoli scientifici più importanti della storia (uno dei più citati a distanza di decenni), la struttura è la seguente
<e0,σ> --> <e0',σ>
----------------------------------------
<e0+e1,σ> --> <e0'+e1,σ>
Negli anni 90 venne introdotta da Gilles Kahn la semantica naturale, dove il risultato è computato in un singolo step
s0 -> r
Al giorno d'oggi, le relazioni di transizione sono tipicamente definite induttivamente, usando assiomi e regole di inferenza usando la sintassi del programma (stile SOS)
Questo formalismo è conveniente perché facilmente traducibile in clausole di Horn in programmazione logica. Inoltre ci sono vantaggi pratici nel fatto che si tratta di una scrittura comprensibile e chiara, in cui ciascuna regola è elegantemente separata.
Idea: il significato di un programma è un oggetto matematico (come una funzione da input ad output) e gli step computazionali usati per valutare il risultato sono poco interessanti
[[.]] : Programmi -> Domini
Ne deriva una chiara semplicità descrittiva, e una ancor più ovvia indipendenza dalle scelte implementative
Fu fondato negli anni 60 da Christopher Stracey e Dana Scott.
Questo formalismo rispetta il principio di composizionalità: le semantiche prendono la forma di una funzione che assegna un elemento appartenente a qualche dominio matematico a ciascun costrutto individuale in maniera tale da non far dipendere il significato dei costrutti dalla forma dei costrutti costituenti, ma solo dai loro significati.
È indubbiamente un formalismo elegante e utilissimo in vari casi:
- trovare comportamenti non specificati/sottospecificati
- utile per derivare implementazioni prototipali
- usato come base di numerosi linguaggi di programmazione
Idea: descrivere i costrutti di un linguaggio provvedendo a fornire assiomi logici soddisfatti da questi costrutti
In tal modo è possibile dimostrare la correttezza di un linguaggio di fronte ad una specifica
⊢ {P} c {Q}
Fu fondata da Floyd (1967) e Hoare (1969)
I vantaggi sono numerosi:
- enfasi sulla correttezza sin dal principio
- notevole eleganza dei sistemi di dimostrazone
- può essere usato per provare l'assenza di bug
Tuttavia tale formalismo trova difficoltà di applicazioni in sistemi interattivi e concorrenti.
Per il resto di questo articolo ci dedicheremo alle semantiche operazionali e denotazionali.
Ora che abbiamo descritto i concetti a fondamento di questi formalismi, definiamo il nostro piccolo linguaggio giocattolo, giusto per farci un'idea di quello con cui stiamo lavorando.
Definiamo una sintassi informale delle espressioni numeriche:
- ogni numerale N è una espressione
- Se E1 e E2 sono espressioni, allora E1⊕E2 è una espressione
- Se E1 e E2 sono espressioni, allora E1⊗E2 è una espressione
La sintassi formale è
E ::= N | E⊕E | E⊗E
⊕3⊗4 non è una espressione ben formata (già scartata a livello di sintassi)
1⊕2⊗3 è un'espressione valida, ma ambigua. Infatti da tale espressione sono derivabili due AST; potremmo risolvere imponendo un certo tipo di precedenza (da sx a dx ecc) o ancora meglio usare le parentesi, ad esempio 1⊕(2⊗3)
È importante notare che la sintassi
E ::= N | E⊕E | E⊗E
non è obbligatoriamente legata a numeri. N può essere qualsiasi cosa. Potremmo star parlando di matrici, con le rispettive definizioni di addizione e moltiplicazione, insiemi con unione ed intersezione o ancora stringhe con concatenazione e l.c.p. ecc.
Questa è solo sintassi!
Notate come abbia utilizzato ⊕ e ⊗ anziché + e ×, proprio per evidenziare il fatto che non mi sto concentrando su una specifica definizione di alcunché.
-2 è valutato come 2 (caso base)
-(1⊕2)⊗3 è valutato come 9
-(1⊕2)⊗(3⊕4) è valutato come 21
È interessante analizzare la semantica small-step, che ammette risultati intermedi con espressioni
- uno step E0 --> E1
- una valutazione E0 --> E1 --> E2 --> ... --> Ek --> n
anche scritta E0 --> n
Ci aspettiamo anche n -/->
Come definire la relazione di transizione?
premesse
------------------(condizione)
conclusione
Se le premesse e la condizione sono entrambe soddisfatte, è possibile trarre la conclusione
Alla sinistra di ciascuna regola è inoltre possibile mettere il nome della regola.
Con un insieme di regole è possibile strutturare la computazione, partendo da regole prive di premesse (assiomi), fino a costruire una catena (anche molto lunga) di regole di inferenza che arrivano infine alla conclusione.